x, y:Top, nms:(MaName List). if [] and nms overlap then x else y fi ~ y 

latex

Definitions	t  T, Id, x:A  B(x), LocKnd, left + right, x:A.B(x), Top, type List, x:AB(x), s = t, x:A. B(x), MaName, l_disjoint(T;l1;l2), False, P  Q, A, P  Q, Dec(P), [], decidable l disjoint manames, f(a), , if p:P then A(p) else B fi , if nms1 and nms2 overlap then x else y fi
Lemmas	top wf, decidable l disjoint manames, MaName wf, decidable wf, l disjoint wf, l disjoint nil, LocKnd wf, Id wf